\documentclass{article} % 声明文档类型为「文章」（适合短篇报告，可选 book/report 等）
\usepackage[UTF8]{ctex} % 加载 ctex 宏包（支持中文），utf8编码
\usepackage{graphicx}
\usepackage{amsmath} % 添加数学包支持

% 自定义 section 编号格式为中文数字
\renewcommand{\thesection}{\chinese{section}}
 % 二级标题用"阿拉伯数字.阿拉伯数字"
\renewcommand{\thesubsection}{\arabic{section}.\arabic{subsection}}


% 文档正文开始（此后内容会被编译显示）
\begin{document} 

\begin{center} % 开启「居中」环境（使内部内容水平居中）
% \tiny（极小）→ \scriptsize → \footnotesize → \small → \normalsize（默认）→ \large → \Large → \LARGE → \huge → \Huge（依次增大）。
% bold font : bf 加粗字体
{\LARGE\textbf{实验二 \ 序列的Z语言基本语法与规则}} \\
\vspace{0.5em} % 增加标题与信息间的垂直间距
\normalsize\textbf{
姓名: \underline{\ \normalfont 李豆豆 \ } \ 
学号: \underline{\ \normalfont 202213216 \ } \ 
专业: \underline{\ \normalfont 软件工程 \ } \
评分: \underline{\ \normalfont \quad \quad \quad }
}
\end{center} % 结束居中环境
% \section{}：一级标题（最大层级，自动加粗并编号）；
% \subsection{}：二级标题（缩进，编号如 1.1）；
% \subsubsection{}：三级标题（进一步缩进，编号如 1.1.1）。
\section{实验目的}  % 一级标题（自动编号为 1 实验目的）
会用LaTex编辑命题逻辑部分的形式化语言，熟悉Z语言推理规则，并生成pdf文件。
\section{实验设备}
可上网计算机。
\section{软件工具的实验内容及步骤}
    \subsection{实验内容：}
        编辑教材第二章(2.3.3)命题逻辑中的推理规则，用LaTex生成PDF文档。
        \begin{enumerate}
            \item 合取：
            \item 析取：
            \item 蕴含：
            \item 等价：
            \item 否定：
            \item 其他：
        \end{enumerate}
        
    \subsection{实验步骤：}
        \begin{enumerate}
        % \wedge 表示 合取，二者皆成立则成立
        % \frac{m1}{m2} 表示从m1推出m2,也就是m1/m2
        % \dfrac 是升级版
            \item 合取：
            % \item \begin{align*} 是 LaTeX 中用于排版多行数学公式的环境，特点是：
            % align 环境用于对齐多行公式
            % * 星号表示不显示公式编号（如果不加星号，每行公式会自动编号）
            % 使用 & 符号来指定对齐点
            % 每行公式用 \\ 来换行
            % [8pt]在每行之前添加适当边距
                \begin{align*}
                    & \dfrac{p \wedge q}{p} && \wedge\text{-elim}_1 \\[8pt]
                    & \dfrac{p \wedge q}{q} && \wedge\text{-elim}_2 \\[8pt]
                    & \dfrac{p,q}{p \wedge q} && \wedge\text{-int} \\[8pt]
                    & \dfrac{\underline{p \wedge p}}{p} && \wedge\text{-id} \\[8pt]
                    & \dfrac{\underline{p \wedge q}}{q \wedge p} && \wedge\text{-com} \\[8pt]
                    & \dfrac{\underline{p \wedge (q \wedge r)}}{(p \wedge q) \wedge r} && \wedge\text{-ass}
                \end{align*}
            \item 析取：
                \begin{align*}
                    & \dfrac{p}{p \vee q} && \vee\text{-int}_1 \\[8pt]
                    & \dfrac{q}{p \vee q} && \vee\text{-int}_2 \\[8pt]
                    & \dfrac{p \vee q,p \Rightarrow r,q \Rightarrow r}{r} && \vee\text{-elim} \\[8pt]
                    & \dfrac{\underline{p \vee p}}{p} && \vee\text{-id} \\[8pt]
                    & \dfrac{\underline{p \vee q}}{q \vee p} && \vee\text{-com} \\[8pt]
                    & \dfrac{\underline{p \vee (q \vee r)}}{(p \vee q) \vee r} && \vee\text{-ass} \\[8pt]
                    & \dfrac{\underline{\neg(\neg p \wedge \neg q)}}{p \vee q} && \vee\text{-equiv}
                \end{align*}
            \item 蕴含：
                % \Rightarrow 表示蕴含符号 ⇒
                % \vdots 表示竖直的省略号
                % \begin{array}{c} 表示一个数组环境，c 表示居中对齐
                \begin{align*}
                    & \dfrac{p \Rightarrow q,p}{q} && \Rightarrow\text{-elim} \\[8pt]
                    & \dfrac{\begin{array}{c} [p] \\ \vdots \\ q \end{array}}{p \Rightarrow q} && \Rightarrow\text{-int} \\[8pt]
                    & \dfrac{\underline{p \Rightarrow q}}{\neg p \vee q} && \Rightarrow\text{-equiv}
                \end{align*}
            \item 等价：
                \begin{align*}
                    & \dfrac{\underline{p \Leftrightarrow q}}{(p \Rightarrow q) \wedge (q \Rightarrow p)} && \Leftrightarrow\text{-equiv} \\[8pt]
                    & \dfrac{\underline{p \Leftrightarrow q}}{p \Rightarrow q} && \Leftrightarrow\text{-elim}_1 \\[8pt]
                    & \dfrac{\underline{p \Leftrightarrow q}}{q \Rightarrow p} && \Leftrightarrow\text{-elim}_2
                \end{align*}
            \item 否定：
                \begin{align*}
                    & \dfrac{\underline{\neg\neg p}}{p} && \text{DN} \\[8pt]
                    & \dfrac{\begin{array}{c} [p] \\ \vdots \\ \neg q \end{array}}{\neg p} && \neg\text{-int}
                \end{align*}
            \item 其他：
                % dist 表示分配律（distributive law）
                % abs 表示吸收律（absorption law）
                \begin{align*}
                    & \dfrac{\underline{p \wedge (q \vee r)}}{(p \wedge q) \vee (p \wedge r)} && \text{dist}_1  \ \ \text{（分配律1）} \\[8pt]
                    & \dfrac{\underline{p \vee (q \wedge r)}}{(p \vee q) \wedge (p \vee r)} && \text{dist}_2  \ \ \text{（分配律2）} \\[8pt]
                    & \dfrac{\underline{p \wedge (p \vee q)}}{p} && \text{abs}_1 \ \ \text{（吸收律1）} \\[8pt]
                    & \dfrac{\underline{p \vee (p \wedge q)}}{p} && \text{abs}_2  \ \ \text{（吸收律2）}
                \end{align*}
        \end{enumerate}
    
    \subsection{实验心得：}
        \indent 在编写推理规则时遇到了几个具体的问题：首先是竖直省略号的处理，最初直接使用 \verb|\\| 换行和 \verb|\vdots| 来表示，但这样会导致括号不匹配的错误。通过查阅资料，发现使用 \verb|\begin{array}{c}| 环境可以很好地处理多行分数中的内容，既保持了格式的美观，又避免了错误。其次是定律名称的中英文混排问题，使用 \verb|\text{}| 命令和 \verb|\ \ | 来添加适当的空格，既确保了数学环境中文本的正确显示，又使得排版更加美观。\\
        \indent 通过这次实验，我学会了 LaTeX 的基本语法和数学公式的排版，更加理解到对于数学领域来说，latex的重要性
\end{document}